;; -*- Mode: Lisp; -*-

;;;; Database for LTRE
;;;; Last Edited: 4/27/94, by KDF

;;; Copyright 1986 - 1995 Kenneth D. Forbus,
;;; Northwestern University, and Johan de Kleer, Xerox Corporation.
;;; All Rights Reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(defpackage #:bps/ltms/ldata
  (:use #:cl
        #:bps/ltms/unify
        #:bps/ltms/linter
        #:bps/ltms/ltms
        #:bps/ltms/funify)
  (:export
   #:dbclass
   #:dbclass-p
   #:dbclass-name
   #:dbclass-ltre
   #:dbclass-facts
   #:dbclass-rules
   #:datum
   #:datum-p
   #:datum-counter
   #:datum-ltre
   #:datum-lisp-form
   #:datum-tms-node
   #:datum-dbclass
   #:datum-assumption?
   #:datum-plist
   #:form<
   #:*connective-list*
   #:simple-proposition?
   #:negated-proposition?
   #:assert!
   #:assume!
   #:already-assumed?
   #:quiet-assert!
   #:rassert!
   #:build-tms-formula
   #:retract!
   #:rretract!
   #:contradiction
   #:assuming
   #:get-dbclass
   #:referent
   #:insert
   #:fetch
   #:get-candidates
   #:map-dbclass
   #:true?
   #:false?
   #:known?
   #:unknown?
   #:label-of
   #:why?
   #:get-tms-node
   #:view-node
   #:signed-view-node
   #:show-datum
   #:make-node-string
   #:assumptions-of
   #:consequences
   #:explore
   #:show-data
   #:get-datum
   #:get-clause
   #:fetch-global
   #:try-rules))

(in-package #:bps/ltms/ldata)

(defstruct (dbclass (:PRINT-FUNCTION dbclass-print-procedure))
  name    ; Corresponding symbol
  ltre    ; LTRE it is part of.
  facts   ; Associated facts
  rules)  ; Associated rules

(defun dbclass-print-procedure (r st ignore)
  (declare (ignore ignore))
  (format st "<Dbclass ~A>" (dbclass-name r)))

(defstruct (datum (:PRINT-FUNCTION datum-print-procedure))
  counter              ; Unique ID for easy lookup
  ltre                 ; The LTRE it is part of
  lisp-form            ; Expression for pattern-matching
  (tms-node nil)       ; Pointer into TMS
  dbclass                ; Dbclass of the corresponding pattern
  (assumption? nil)    ; if non-nil, indicates informant
  (plist nil))          ; local property list

(defun datum-print-procedure (d st ignore)
  (declare (ignore ignore))
  (format st "<Datum ~D>" (datum-counter d)))

;; Previous version used ALPHALESSP, a refuge from MACLISP that
;; compared the printed representations of any two lisp objects (as
;; defined by FORMAT.  Given that we only use it for database forms,
;; exploiting the datum counter to provide a cheap ordering constraint
;; between assertions makes more sense.

(defun form< (x y) (< (datum-counter (referent x t))
                      (datum-counter (referent y t))))


;;;; Adding data

(defvar *connective-list* '(:IMPLIES :AND :OR :IFF :NOT :TAXONOMY))

(defun simple-proposition? (x)
  (or (not (listp x))
      (not (member (car x) *connective-list*))))

(defun negated-proposition? (form)
  (and (listp form) (eq (car form) :NOT)
       (simple-proposition? (cadr form))))

(defun assert! (fact just &optional (*LTRE* *LTRE*))
  (debugging-ltre "~%    Asserting ~A via ~A." fact just)
  ;; For assertions, simply install the clause.
  (add-formula (ltre-ltms *ltre*) (build-tms-formula fact *LTRE*) just))

(defun assume! (fact reason &optional (*LTRE* *LTRE*) &aux datum node)
  (setq datum (referent (if (negated-proposition? fact) (cadr fact)
                          fact) t)
        node (datum-tms-node datum))
  (debugging-ltre "~%    Assuming ~A via ~A." fact reason)
  (unless (or (negated-proposition? fact) (simple-proposition? fact))
          ;; Install clauses corresponding to the assumption, with proper
          ;; logical scoping
          (add-formula (ltre-ltms *ltre*)
             `(:IMPLIES ,node ,(build-tms-formula fact *LTRE*)) reason))
  (cond ((not (datum-assumption? datum))
         (setf (datum-assumption? datum) reason)
         (convert-to-assumption node)
         (enable-assumption node (if (negated-proposition? fact) :FALSE :TRUE)))
        ((eq reason (datum-assumption? datum)))
        (t (error "Fact ~A assumed because of ~A assumed again because of ~A"
                  (show-datum datum) (datum-assumption? datum) reason)))
  datum)

(defun already-assumed? (fact)
  (datum-assumption? (referent fact t)))

(defun quiet-assert! (fact *LTRE* &optional (just 'user))
  (without-contradiction-check (ltre-ltms *LTRE*)
    (assert! fact *LTRE* just)))

(defmacro rassert! (fact &optional (just 'user))
  `(assert! ,(quotize fact) ,(quotize just)))

(defun build-tms-formula (formula *LTRE*)
  (cond ((and (listp formula)
              (member (car formula) *connective-list*))
         (cons (car formula)
               (mapcar #'(lambda (form)
                           (build-tms-formula form *LTRE*)) (cdr formula))))
        (t (datum-tms-node (referent formula t)))))

;;; Retraction and "bulk assumptions"

(defun retract! (fact just &optional (*LTRE* *LTRE*) (quiet? t)
                      &aux datum node)
  (setq datum (referent fact t)
        node (datum-tms-node datum))
  (cond ((not (tms-node-assumption? node))
         (unless quiet?
           (format t "~%~A isn't an assumption." (show-datum datum))))
        ((not (known-node? node))
         (unless quiet?
           (format T "~%The assumption ~A is not currently in." fact)))
        ((eq just (datum-assumption? datum))
         (debugging-ltre "~%    Retracting ~A via ~A." fact just)
         (setf (datum-assumption? datum) nil)
         (retract-assumption node))
        ((not quiet?)
         (format t "~%~A not source of assumption for ~A"
                 just fact)))
  node)

(defmacro rretract! (fact &optional (just 'USER))
  `(retract! ,(quotize fact) ,(quotize just)))

(defun contradiction (losers *LTRE* &aux datum trues falses)
  ;; Here we re-cycle this procedure to indicate that a
  ;; conjunction of facts are contradictory.
  (dolist (fact losers
                (add-clause trues falses :DECLARED-CONTRADICTION))
    (setq datum (referent fact t))
    (if (negated-proposition? fact)
        (push (datum-tms-node datum) falses)
      (push (datum-tms-node datum) trues))))

(defmacro assuming (facts-to-assume *LTRE* &body body)
  ;; A useful abstraction for user code.
  `(with-assumptions
    (mapcar #'(lambda (fact &aux node datum)
                (setq datum (referent fact t)
                      node (datum-tms-node datum))
                (convert-to-assumption node)
                (cons node (if (negated-proposition? fact) :FALSE :TRUE)))
            ,facts-to-assume)
    ,@ body))

;;;; Database system

(defun get-dbclass (fact &optional (*LTRE* *LTRE*) &aux dbclass)
  (cond ((null fact) (error "~% NIL can't be a dbclass."))
        ((listp fact)
         (cond ((negated-proposition? fact) (get-dbclass (cadr fact) *LTRE*))
               (t (get-dbclass (car fact) *LTRE*))))
        ((variable? fact)
         (cond ((boundp fact) (get-dbclass (symbol-value fact) *LTRE*))
               (t (error "~%Dbclass unbound: ~A" fact))))
        ((symbolp fact)
         (cond ((gethash fact (ltre-dbclass-table *LTRE*)))
               (t (setq dbclass
                        (make-dbclass :NAME fact :FACTS nil
                                    :RULES nil :LTRE *LTRE*))
                  (setf (gethash fact (ltre-dbclass-table *LTRE*)) dbclass)
                  dbclass)))
        (t (error "Bad dbclass type: ~A" fact))))

(defun referent (fact &optional (virtual? nil) (*LTRE* *LTRE*))
  (if virtual? (insert fact) (referent1 fact)))

(defun referent1 (fact &aux form) ;; Could use seperate hash table
  (setq form (if (negated-proposition? fact) (cadr fact) fact))
  (dolist (candidate (dbclass-facts (get-dbclass fact *LTRE*)))
          (when (equal (datum-lisp-form candidate) form)
                (return candidate))))

(defun insert (fact &aux datum form)
  (setq datum (referent1 fact))
  (cond (datum (values datum t))
        (t (setq form (if (negated-proposition? fact) (cadr fact) fact))
           (setq datum (make-datum :COUNTER (incf (ltre-datum-counter *LTRE*))
                                   :LTRE *LTRE*
                                   :LISP-FORM form
                                   :DBCLASS (get-dbclass form *LTRE*)))
           (setf (datum-tms-node datum) (tms-create-node (ltre-ltms *LTRE*) datum))
           (push datum (dbclass-facts (datum-dbclass datum)))
           (try-rules datum)
           (values datum nil))))

(defun fetch (pattern &optional (*LTRE* *LTRE*) &aux bindings unifiers form)
  (setq form (if (negated-proposition? pattern) (cadr pattern) pattern))
  (dolist (candidate (get-candidates form *LTRE*) unifiers)
    (setq bindings (unify form (datum-lisp-form candidate)))
    (unless (eq bindings :FAIL)
      (push (sublis bindings pattern) unifiers))))

(defun get-candidates (pattern *LTRE*)
  (dbclass-facts (get-dbclass pattern *LTRE*)))

(defun map-dbclass (proc &optional (*LTRE* *LTRE*))
  (maphash #'(lambda (name dbclass) (declare (ignore name))
               (funcall proc dbclass))
           (ltre-dbclass-table *LTRE*)))

;;;; Interface and display of data

(defun true? (fact &optional (*LTRE* *LTRE*) &aux r)
  (when (setq r (referent fact nil))
    (if (negated-proposition? fact)
        (false-node? (datum-tms-node r))
        (true-node? (datum-tms-node r)))))

(defun false? (fact &optional (*LTRE* *LTRE*) &aux r)
  (when (setq r (referent fact nil))
    (if (negated-proposition? fact)
        (true-node? (datum-tms-node r))
        (false-node? (datum-tms-node r)))))

(defun known? (fact &optional (*LTRE* *LTRE*) &aux r)
  (when (setq r (referent fact nil))
    (known-node? (datum-tms-node r))))

(defun unknown? (fact &optional (*LTRE* *LTRE*) &aux r)
  (if (setq r (referent fact nil))
      (unknown-node? (datum-tms-node r))
      t))

(defun label-of (fact &optional (*ltre* *ltre*) &aux r)
  (when (setq r (referent fact nil))
        (tms-node-label (datum-tms-node r))))

(defun why? (fact &optional (*LTRE* *LTRE*) &aux r)
  (cond ((setq r (referent fact nil))
         (why-node (datum-tms-node r))
         (if (and (known-node? (datum-tms-node r))
                  (datum-assumption? r))
             (format t " (~A)" (datum-assumption? r))))
        (t (format t "~%~A not in database." fact))))

(defun get-tms-node (fact &optional (*LTRE* *LTRE*))
  (datum-tms-node (referent fact t)))

(defun view-node (d)
  (datum-lisp-form (tms-node-datum d)))

(defun signed-view-node (d) ;; For creating terms in clauses
  (if (false-node? d) (list :NOT (view-node d))
    (if (true-node? d) (view-node d)
      (error "SIGNED-VIEW-NODE requires knowing label: ~A" d))))

(defun show-datum (datum) (format nil "~A" (datum-lisp-form datum)))
(defun make-node-string (node) (show-datum (tms-node-datum node))) ;; For LTMS

(defun assumptions-of (fact &optional (*LTRE* *LTRE*))
  (mapcar #'view-node
          (assumptions-of-node
           (datum-tms-node (referent fact t)))))

(defun consequences (fact)
  (unless (known? fact) (return-from consequences nil))
  (show-node-consequences (get-tms-node fact)))

(defun explore (fact) (explore-network (get-tms-node fact)))

;;;; Global interrogatives

(defun show-data (&optional (*LTRE* *LTRE*) (stream *standard-output*)
                            &aux counter)
  (setq counter 0)
  (format stream
          "~%~D facts total." (ltre-datum-counter *LTRE*))
  (maphash
   #'(lambda (key dbclass)
       (declare (ignore key))
       (dolist (datum (dbclass-facts dbclass))
         (incf counter)
         (format stream "~%~A: ~A" (show-datum datum)
                 (cond ((true-node? (datum-tms-node datum)) "TRUE")
                       ((false-node? (datum-tms-node datum)) "FALSE")
                       (t "UNKNOWN")))))
   (ltre-dbclass-table *LTRE*))
  counter)

(defun get-datum (num &optional (*LTRE* *LTRE*))
  (maphash #'(lambda (key dbclass)
               (declare (ignore key))
               (dolist (datum (dbclass-facts dbclass))
                       (when (= (datum-counter datum) num)
                             (return-from GET-DATUM datum))))
           (ltre-dbclass-table *LTRE*)))

(defun get-clause (num &optional (*LTRE* *LTRE*))
  (dolist (clause (ltms-clauses (ltre-ltms *LTRE*)))
    (when (= (clause-index clause) num) (return-from GET-clause clause))))

(defun fetch-global (pattern &optional (status nil) (*ltre* *ltre*)
                             &aux results)
  (map-dbclass
   #'(lambda (dbclass)
       (dolist (datum (dbclass-facts dbclass))
               (if (and (case status
                              (:TRUE (true-node? (datum-tms-node datum)))
                              (:FALSE (false-node? (datum-tms-node datum)))
                              (:KNOWN (known-node? (datum-tms-node datum)))
                              (:UNKNOWN (not (known-node? (datum-tms-node datum))))
                              (t t))
                        (not (eq (unify (datum-lisp-form datum) pattern) :FAIL)))
                   (push (datum-lisp-form datum) results)))))
  results)
